Library daleth_conjugate
Require Import PointsETC.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition daleth_conjugate P U :=
match P,U with
cTriple p q r, cTriple u v w ⇒
let h p q r u v w := p×(v/q - w/r)^2 + u*(2×u/p - v/q - w/r) in
cTriple (h p q r u v w) (h q r p v w u) (h r p q w u v)
end.
Lemma X1_is_daleth_conjugate_of_X1_X44 :
eq_points X_1 (daleth_conjugate X_1 X_44).
Proof.
intros.
red;simpl; repeat split; field; repeat split;auto with triangle_hyps.
Qed.
End Triangle.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition daleth_conjugate P U :=
match P,U with
cTriple p q r, cTriple u v w ⇒
let h p q r u v w := p×(v/q - w/r)^2 + u*(2×u/p - v/q - w/r) in
cTriple (h p q r u v w) (h q r p v w u) (h r p q w u v)
end.
Lemma X1_is_daleth_conjugate_of_X1_X44 :
eq_points X_1 (daleth_conjugate X_1 X_44).
Proof.
intros.
red;simpl; repeat split; field; repeat split;auto with triangle_hyps.
Qed.
End Triangle.